open import Level using ( Level ; _⊔_ ; suc )
open import Relation.Binary using ( Rel )
open import Relation.Unary using ( Pred ; U; Decidable )
open import Algebra.FunctionProperties using ( Op₁ ; Op₂ )
open import Data.Product using ( _×_ ; _,′_ ; Σ ; _,_; proj₂ ; proj₁) 
open import Substructures using (SubGroup ; IsSubGroup; IsNormalSubGroup ; NormalSubGroup)
open import Function using (_$_ ; _∘_)
import Algebra.Properties.Group as GroupProperties
import Relation.Binary.EqReasoning as EqR

module Coset where

private 
  xCoset : {a b ℓ : Level} {A : Set a} (_≈_ : Rel A ℓ) (subsetPred : Pred A b) (_∙_ : Op₂ A) (g : A) (whichOne : (h : A) → {_ : subsetPred h} → A )  → (Pred A (a ⊔ (b ⊔ ℓ)))
  xCoset {A = A} _≈_ subsetPred _∙_  g which x = Σ A (λ h → Σ (subsetPred h) (λ hP → x ≈ (which h {hP})))
leftCosetPred : {a b ℓ : Level} {A : Set a} (_≈_ : Rel A ℓ) (subsetPred : Pred A b) (_∙_ : Op₂ A)  (g : A) → (Pred A (a ⊔ (b ⊔ ℓ)))
leftCosetPred _≈_ subsetPred _∙_ g = xCoset _≈_ subsetPred _∙_ g (λ h  → g ∙ h)
rightCosetPred : {a b ℓ : Level} {A : Set a} (_≈_ : Rel A ℓ) (subsetPred : Pred A b) (_∙_ : Op₂ A) (g : A) → (Pred A (a ⊔ (b ⊔ ℓ)))
rightCosetPred _≈_ subsetPred _∙_ g = xCoset _≈_ subsetPred _∙_ g (λ h → h ∙ g)

normalGroup⇒cosetsEq : {a b ℓ : Level} {A : Set a} (_≈_ : Rel A ℓ)
  (subsetPred : Pred A b) (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) 
  (isNormalSubGroup : IsNormalSubGroup _≈_ subsetPred _∙_ ε _⁻¹) → (g : A) →
  (x : A) → 
  let
    leftCosetP =  leftCosetPred _≈_ subsetPred _∙_ g
    rightCosetP = rightCosetPred _≈_ subsetPred _∙_ g
    l→r = leftCosetP x → rightCosetP x
    r→l = rightCosetP x → leftCosetP x
  in (l→r × r→l) -- Uwaga: to nie musi być biekcja! (tzn: l→r $ r→l ≠ x→x)
normalGroup⇒cosetsEq {A = A} _≈_ subsetPred _∙_ ε _⁻¹ isNormalSubGroup g x =
  let open IsNormalSubGroup isNormalSubGroup in let open EqR setoid in let
    leftCosetP =  leftCosetPred _≈_ subsetPred _∙_ g
    rightCosetP = rightCosetPred _≈_ subsetPred _∙_ g
    l→r : leftCosetP x → rightCosetP x
    l→r lP = let
      h = proj₁ lP
      hP = proj₁ ∘ proj₂ $ lP
      x≈gh : x ≈ (g ∙ h)
      x≈gh =  proj₂ ∘ proj₂ $ lP
      transformation : x ≈ (((g ∙ h) ∙ (g ⁻¹)) ∙ g)
      transformation = begin
        x ≈⟨ x≈gh ⟩
        (g ∙ h) ≈⟨ sym $ identityʳ _ ⟩
        (g ∙ h) ∙ ε ≈⟨  ∙-cong refl (sym $ inverseˡ g) ⟩
        (g ∙ h) ∙ ((g ⁻¹) ∙ g) ≈⟨ sym $ assoc _ _ _ ⟩
        ((g ∙ h) ∙ (g ⁻¹)) ∙ g ∎
      in ((g ∙ h) ∙ (g ⁻¹)) , isNormal g h hP , transformation
    open GroupProperties (record -- te kilka wierszy jest tylko po ⁻¹-involutive ლ(ಠ益ಠლ)
                            { Carrier = A
                            ; _≈_ = _≈_
                            ; _∙_ = _∙_
                            ; ε = ε
                            ; _⁻¹ = _⁻¹
                            ; isGroup = isGroup
                            })
    r→l : rightCosetP x → leftCosetP x
    r→l rP = let
        h = proj₁ rP
        hP = proj₁ ∘ proj₂ $ rP
        x≈hg : x ≈ (h ∙ g)
        x≈hg = proj₂ ∘ proj₂ $ rP
        transformation = begin
          x ≈⟨ x≈hg ⟩
          h ∙ g ≈⟨ sym $ identityˡ _ ⟩ 
          ε ∙ (h ∙ g) ≈⟨ ∙-cong (sym $ inverseʳ _) refl ⟩
          (g ∙ (g ⁻¹)) ∙ (h ∙ g) ≈⟨ assoc _ _ _ ⟩
          g ∙ ((g ⁻¹) ∙ (h ∙ g)) ∎
        predFulfilment : subsetPred ((g ⁻¹) ∙ (h ∙ g))
        predFulfilment = ≈_respect
          (begin
            ((g ⁻¹) ∙ h) ∙ ((g ⁻¹ ) ⁻¹ ) ≈⟨ assoc _ _ _ ⟩
            (g ⁻¹) ∙ (h ∙ ((g ⁻¹ ) ⁻¹ )) ≈⟨ ∙-cong refl (∙-cong refl (⁻¹-involutive _)) ⟩ 
            ((g ⁻¹) ∙ (h ∙ g)) ∎)
          (isNormal (g ⁻¹) h hP)
        in ((g ⁻¹) ∙ (h ∙ g)) , (predFulfilment , transformation)
  in
  l→r , r→l
